; taken from https://github.com/z3str/Z3-str/tree/master/benchmark

(set-logic QF_S)

(declare-fun I0_16 () Int)
(declare-fun I0_2 () Int)
(declare-fun I0_21 () Int)
(declare-fun I0_25 () Int)
(declare-fun I0_35 () Int)
(declare-fun I0_4 () Int)
(declare-fun I0_8 () Int)
(declare-fun I1_21 () Int)
(declare-fun I1_25 () Int)
(declare-fun I1_8 () Int)
(declare-fun I2_21 () Int)
(declare-fun I2_25 () Int)
(declare-fun I2_8 () Int)
(declare-fun M0_10 () String)
(declare-fun M10_10 () String)
(declare-fun M11_10 () String)
(declare-fun M12_10 () String)
(declare-fun M13_10 () String)
(declare-fun M14_10 () String)
(declare-fun M15_10 () String)
(declare-fun M16_10 () String)
(declare-fun M17_10 () String)
(declare-fun M18_10 () String)
(declare-fun M19_10 () String)
(declare-fun M1_10 () String)
(declare-fun M20_10 () String)
(declare-fun M21_10 () String)
(declare-fun M22_10 () String)
(declare-fun M23_10 () String)
(declare-fun M24_10 () String)
(declare-fun M2_10 () String)
(declare-fun M3_10 () String)
(declare-fun M4_10 () String)
(declare-fun M5_10 () String)
(declare-fun M6_10 () String)
(declare-fun M7_10 () String)
(declare-fun M8_10 () String)
(declare-fun M9_10 () String)
(declare-fun P0_10 () String)
(declare-fun P10_10 () String)
(declare-fun P11_10 () String)
(declare-fun P12_10 () String)
(declare-fun P13_10 () String)
(declare-fun P14_10 () String)
(declare-fun P15_10 () String)
(declare-fun P16_10 () String)
(declare-fun P17_10 () String)
(declare-fun P18_10 () String)
(declare-fun P19_10 () String)
(declare-fun P1_10 () String)
(declare-fun P20_10 () String)
(declare-fun P21_10 () String)
(declare-fun P22_10 () String)
(declare-fun P23_10 () String)
(declare-fun P24_10 () String)
(declare-fun P2_10 () String)
(declare-fun P3_10 () String)
(declare-fun P4_10 () String)
(declare-fun P5_10 () String)
(declare-fun P6_10 () String)
(declare-fun P7_10 () String)
(declare-fun P8_10 () String)
(declare-fun P9_10 () String)
(declare-fun PCTEMP_LHS_1 () Int)
(declare-fun PCTEMP_LHS_10 () Int)
(declare-fun PCTEMP_LHS_2 () Int)
(declare-fun PCTEMP_LHS_3 () String)
(declare-fun PCTEMP_LHS_4 () String)
(declare-fun PCTEMP_LHS_4_idx_0 () String)
(declare-fun PCTEMP_LHS_4_idx_1 () String)
(declare-fun PCTEMP_LHS_4_idx_10 () String)
(declare-fun PCTEMP_LHS_4_idx_11 () String)
(declare-fun PCTEMP_LHS_4_idx_12 () String)
(declare-fun PCTEMP_LHS_4_idx_13 () String)
(declare-fun PCTEMP_LHS_4_idx_14 () String)
(declare-fun PCTEMP_LHS_4_idx_15 () String)
(declare-fun PCTEMP_LHS_4_idx_16 () String)
(declare-fun PCTEMP_LHS_4_idx_17 () String)
(declare-fun PCTEMP_LHS_4_idx_18 () String)
(declare-fun PCTEMP_LHS_4_idx_19 () String)
(declare-fun PCTEMP_LHS_4_idx_2 () String)
(declare-fun PCTEMP_LHS_4_idx_20 () String)
(declare-fun PCTEMP_LHS_4_idx_21 () String)
(declare-fun PCTEMP_LHS_4_idx_22 () String)
(declare-fun PCTEMP_LHS_4_idx_23 () String)
(declare-fun PCTEMP_LHS_4_idx_24 () String)
(declare-fun PCTEMP_LHS_4_idx_25 () String)
(declare-fun PCTEMP_LHS_4_idx_3 () String)
(declare-fun PCTEMP_LHS_4_idx_4 () String)
(declare-fun PCTEMP_LHS_4_idx_5 () String)
(declare-fun PCTEMP_LHS_4_idx_6 () String)
(declare-fun PCTEMP_LHS_4_idx_7 () String)
(declare-fun PCTEMP_LHS_4_idx_8 () String)
(declare-fun PCTEMP_LHS_4_idx_9 () String)
(declare-fun PCTEMP_LHS_5 () Int)
(declare-fun PCTEMP_LHS_6 () String)
(declare-fun PCTEMP_LHS_7 () String)
(declare-fun PCTEMP_LHS_8 () String)
(declare-fun PCTEMP_LHS_9 () String)
(declare-fun T0_10 () String)
(declare-fun T0_16 () String)
(declare-fun T0_2 () String)
(declare-fun T0_35 () String)
(declare-fun T0_4 () String)
(declare-fun T10_10 () String)
(declare-fun T11_10 () String)
(declare-fun T12_10 () String)
(declare-fun T13_10 () String)
(declare-fun T14_10 () String)
(declare-fun T15_10 () String)
(declare-fun T16_10 () String)
(declare-fun T17_10 () String)
(declare-fun T18_10 () String)
(declare-fun T19_10 () String)
(declare-fun T1_10 () String)
(declare-fun T1_16 () String)
(declare-fun T1_2 () String)
(declare-fun T1_21 () String)
(declare-fun T1_25 () String)
(declare-fun T1_35 () String)
(declare-fun T1_4 () String)
(declare-fun T1_8 () String)
(declare-fun T20_10 () String)
(declare-fun T21_10 () String)
(declare-fun T22_10 () String)
(declare-fun T23_10 () String)
(declare-fun T24_10 () String)
(declare-fun T25_10 () String)
(declare-fun T2_10 () String)
(declare-fun T2_16 () String)
(declare-fun T2_2 () String)
(declare-fun T2_21 () String)
(declare-fun T2_25 () String)
(declare-fun T2_35 () String)
(declare-fun T2_4 () String)
(declare-fun T2_8 () String)
(declare-fun T3_10 () String)
(declare-fun T3_16 () String)
(declare-fun T3_2 () String)
(declare-fun T3_21 () String)
(declare-fun T3_25 () String)
(declare-fun T3_35 () String)
(declare-fun T3_4 () String)
(declare-fun T3_8 () String)
(declare-fun T4_10 () String)
(declare-fun T4_16 () String)
(declare-fun T4_2 () String)
(declare-fun T4_35 () String)
(declare-fun T4_4 () String)
(declare-fun T5_10 () String)
(declare-fun T5_16 () String)
(declare-fun T5_2 () String)
(declare-fun T5_35 () String)
(declare-fun T5_4 () String)
(declare-fun T6_10 () String)
(declare-fun T7_10 () String)
(declare-fun T8_10 () String)
(declare-fun T9_10 () String)
(declare-fun T_10 () Int)
(declare-fun T_14 () Int)
(declare-fun T_15 () Bool)
(declare-fun T_16 () String)
(declare-fun T_18 () Bool)
(declare-fun T_3 () Bool)
(declare-fun T_4 () Int)
(declare-fun T_7 () Int)
(declare-fun T_8 () Bool)
(declare-fun T_9 () String)
(declare-fun T_SELECT_1 () Bool)
(declare-fun T_SELECT_2 () Bool)
(declare-fun T_SELECT_3 () Bool)
(declare-fun T_SELECT_4 () Bool)
(declare-fun T_b () Bool)
(declare-fun T_c () Bool)
(declare-fun T_d () String)
(declare-fun T_f () String)
(declare-fun var_0xINPUT_311 () String)

(assert (= T_SELECT_1 (not (= PCTEMP_LHS_1 (- 1)))))
(assert (ite T_SELECT_1
	(and (= PCTEMP_LHS_1 (+ I0_2 0))(= var_0xINPUT_311 (str.++ T0_2 T1_2))(= I0_2 (str.len T4_2))(= 0 (str.len T0_2))(= T1_2 (str.++ T2_2 T3_2))(= T2_2 (str.++ T4_2 T5_2))(= T5_2 "?")(not (str.in.re T4_2 (str.to.re "?"))))
	(and (= PCTEMP_LHS_1 (- 1))(= var_0xINPUT_311 (str.++ T0_2 T1_2))(= 0 (str.len T0_2))(not (str.in.re T1_2 (str.to.re "?"))))))
(assert (= T_SELECT_2 (not (= PCTEMP_LHS_2 (- 1)))))
(assert (ite T_SELECT_2
	(and (= PCTEMP_LHS_2 (+ I0_4 0))(= var_0xINPUT_311 (str.++ T0_4 T1_4))(= I0_4 (str.len T4_4))(= 0 (str.len T0_4))(= T1_4 (str.++ T2_4 T3_4))(= T2_4 (str.++ T4_4 T5_4))(= T5_4 "#")(not (str.in.re T4_4 (str.to.re "#"))))
	(and (= PCTEMP_LHS_2 (- 1))(= var_0xINPUT_311 (str.++ T0_4 T1_4))(= 0 (str.len T0_4))(not (str.in.re T1_4 (str.to.re "#"))))))
(assert (= T_3 (= PCTEMP_LHS_2 (- 1))))
(assert T_3)
(assert (= T_4 (+ PCTEMP_LHS_1 1)))
(assert (= I0_8 (- I2_8 T_4)))
(assert (>= T_4 0))
(assert (>= I2_8 T_4))
(assert (<= I2_8 I1_8))
(assert (= I2_8 I1_8))
(assert (= I0_8 (str.len PCTEMP_LHS_3)))
(assert (= var_0xINPUT_311 (str.++ T1_8 T2_8)))
(assert (= T2_8 (str.++ PCTEMP_LHS_3 T3_8)))
(assert (= T_4 (str.len T1_8)))
(assert (= I1_8 (str.len var_0xINPUT_311)))
(assert (= T25_10 PCTEMP_LHS_4_idx_25))
(assert (= T0_10 PCTEMP_LHS_3))
(assert (= M24_10 "&"))
(assert (not (str.in.re PCTEMP_LHS_4_idx_24 (str.to.re "&"))))
(assert (= P24_10 (str.++ PCTEMP_LHS_4_idx_24 M24_10)))
(assert (= T24_10 (str.++ P24_10 T25_10)))
(assert (= M23_10 "&"))
(assert (not (str.in.re PCTEMP_LHS_4_idx_23 (str.to.re "&"))))
(assert (= P23_10 (str.++ PCTEMP_LHS_4_idx_23 M23_10)))
(assert (= T23_10 (str.++ P23_10 T24_10)))
(assert (= M22_10 "&"))
(assert (not (str.in.re PCTEMP_LHS_4_idx_22 (str.to.re "&"))))
(assert (= P22_10 (str.++ PCTEMP_LHS_4_idx_22 M22_10)))
(assert (= T22_10 (str.++ P22_10 T23_10)))
(assert (= M21_10 "&"))
(assert (not (str.in.re PCTEMP_LHS_4_idx_21 (str.to.re "&"))))
(assert (= P21_10 (str.++ PCTEMP_LHS_4_idx_21 M21_10)))
(assert (= T21_10 (str.++ P21_10 T22_10)))
(assert (= M20_10 "&"))
(assert (not (str.in.re PCTEMP_LHS_4_idx_20 (str.to.re "&"))))
(assert (= P20_10 (str.++ PCTEMP_LHS_4_idx_20 M20_10)))
(assert (= T20_10 (str.++ P20_10 T21_10)))
(assert (= M19_10 "&"))
(assert (not (str.in.re PCTEMP_LHS_4_idx_19 (str.to.re "&"))))
(assert (= P19_10 (str.++ PCTEMP_LHS_4_idx_19 M19_10)))
(assert (= T19_10 (str.++ P19_10 T20_10)))
(assert (= M18_10 "&"))
(assert (not (str.in.re PCTEMP_LHS_4_idx_18 (str.to.re "&"))))
(assert (= P18_10 (str.++ PCTEMP_LHS_4_idx_18 M18_10)))
(assert (= T18_10 (str.++ P18_10 T19_10)))
(assert (= M17_10 "&"))
(assert (not (str.in.re PCTEMP_LHS_4_idx_17 (str.to.re "&"))))
(assert (= P17_10 (str.++ PCTEMP_LHS_4_idx_17 M17_10)))
(assert (= T17_10 (str.++ P17_10 T18_10)))
(assert (= M16_10 "&"))
(assert (not (str.in.re PCTEMP_LHS_4_idx_16 (str.to.re "&"))))
(assert (= P16_10 (str.++ PCTEMP_LHS_4_idx_16 M16_10)))
(assert (= T16_10 (str.++ P16_10 T17_10)))
(assert (= M15_10 "&"))
(assert (not (str.in.re PCTEMP_LHS_4_idx_15 (str.to.re "&"))))
(assert (= P15_10 (str.++ PCTEMP_LHS_4_idx_15 M15_10)))
(assert (= T15_10 (str.++ P15_10 T16_10)))
(assert (= M14_10 "&"))
(assert (not (str.in.re PCTEMP_LHS_4_idx_14 (str.to.re "&"))))
(assert (= P14_10 (str.++ PCTEMP_LHS_4_idx_14 M14_10)))
(assert (= T14_10 (str.++ P14_10 T15_10)))
(assert (= M13_10 "&"))
(assert (not (str.in.re PCTEMP_LHS_4_idx_13 (str.to.re "&"))))
(assert (= P13_10 (str.++ PCTEMP_LHS_4_idx_13 M13_10)))
(assert (= T13_10 (str.++ P13_10 T14_10)))
(assert (= M12_10 "&"))
(assert (not (str.in.re PCTEMP_LHS_4_idx_12 (str.to.re "&"))))
(assert (= P12_10 (str.++ PCTEMP_LHS_4_idx_12 M12_10)))
(assert (= T12_10 (str.++ P12_10 T13_10)))
(assert (= M11_10 "&"))
(assert (not (str.in.re PCTEMP_LHS_4_idx_11 (str.to.re "&"))))
(assert (= P11_10 (str.++ PCTEMP_LHS_4_idx_11 M11_10)))
(assert (= T11_10 (str.++ P11_10 T12_10)))
(assert (= M10_10 "&"))
(assert (not (str.in.re PCTEMP_LHS_4_idx_10 (str.to.re "&"))))
(assert (= P10_10 (str.++ PCTEMP_LHS_4_idx_10 M10_10)))
(assert (= T10_10 (str.++ P10_10 T11_10)))
(assert (= M9_10 "&"))
(assert (not (str.in.re PCTEMP_LHS_4_idx_9 (str.to.re "&"))))
(assert (= P9_10 (str.++ PCTEMP_LHS_4_idx_9 M9_10)))
(assert (= T9_10 (str.++ P9_10 T10_10)))
(assert (= M8_10 "&"))
(assert (not (str.in.re PCTEMP_LHS_4_idx_8 (str.to.re "&"))))
(assert (= P8_10 (str.++ PCTEMP_LHS_4_idx_8 M8_10)))
(assert (= T8_10 (str.++ P8_10 T9_10)))
(assert (= M7_10 "&"))
(assert (not (str.in.re PCTEMP_LHS_4_idx_7 (str.to.re "&"))))
(assert (= P7_10 (str.++ PCTEMP_LHS_4_idx_7 M7_10)))
(assert (= T7_10 (str.++ P7_10 T8_10)))
(assert (= M6_10 "&"))
(assert (not (str.in.re PCTEMP_LHS_4_idx_6 (str.to.re "&"))))
(assert (= P6_10 (str.++ PCTEMP_LHS_4_idx_6 M6_10)))
(assert (= T6_10 (str.++ P6_10 T7_10)))
(assert (= M5_10 "&"))
(assert (not (str.in.re PCTEMP_LHS_4_idx_5 (str.to.re "&"))))
(assert (= P5_10 (str.++ PCTEMP_LHS_4_idx_5 M5_10)))
(assert (= T5_10 (str.++ P5_10 T6_10)))
(assert (= M4_10 "&"))
(assert (not (str.in.re PCTEMP_LHS_4_idx_4 (str.to.re "&"))))
(assert (= P4_10 (str.++ PCTEMP_LHS_4_idx_4 M4_10)))
(assert (= T4_10 (str.++ P4_10 T5_10)))
(assert (= M3_10 "&"))
(assert (not (str.in.re PCTEMP_LHS_4_idx_3 (str.to.re "&"))))
(assert (= P3_10 (str.++ PCTEMP_LHS_4_idx_3 M3_10)))
(assert (= T3_10 (str.++ P3_10 T4_10)))
(assert (= M2_10 "&"))
(assert (not (str.in.re PCTEMP_LHS_4_idx_2 (str.to.re "&"))))
(assert (= P2_10 (str.++ PCTEMP_LHS_4_idx_2 M2_10)))
(assert (= T2_10 (str.++ P2_10 T3_10)))
(assert (= M1_10 "&"))
(assert (not (str.in.re PCTEMP_LHS_4_idx_1 (str.to.re "&"))))
(assert (= P1_10 (str.++ PCTEMP_LHS_4_idx_1 M1_10)))
(assert (= T1_10 (str.++ P1_10 T2_10)))
(assert (= M0_10 "&"))
(assert (not (str.in.re PCTEMP_LHS_4_idx_0 (str.to.re "&"))))
(assert (= P0_10 (str.++ PCTEMP_LHS_4_idx_0 M0_10)))
(assert (= T0_10 (str.++ P0_10 T1_10)))
(assert (= T_7 (str.len PCTEMP_LHS_4)))
(assert (= T_8 (< 0 T_7)))
(assert T_8)
(assert (= T_9 PCTEMP_LHS_4_idx_0))
(assert (= T_SELECT_3 (not (= PCTEMP_LHS_5 (- 1)))))
(assert (ite T_SELECT_3
	(and (= PCTEMP_LHS_5 (+ I0_16 0))(= T_9 (str.++ T0_16 T1_16))(= I0_16 (str.len T4_16))(= 0 (str.len T0_16))(= T1_16 (str.++ T2_16 T3_16))(= T2_16 (str.++ T4_16 T5_16))(= T5_16 "=")(not (str.in.re T4_16 (str.to.re "="))))
	(and (= PCTEMP_LHS_5 (- 1))(= T_9 (str.++ T0_16 T1_16))(= 0 (str.len T0_16))(not (str.in.re T1_16 (str.to.re "="""))))))
(assert (= T_b (= PCTEMP_LHS_5 (- 1))))
(assert (= T_c (not T_b)))
(assert T_c)
(assert (= T_d PCTEMP_LHS_4_idx_0))
(assert (= I0_21 (- PCTEMP_LHS_5 0)))
(assert (>= 0 0))
(assert (>= PCTEMP_LHS_5 0))
(assert (<= PCTEMP_LHS_5 I1_21))
(assert (= I2_21 I1_21))
(assert (= I0_21 (str.len PCTEMP_LHS_6)))
(assert (= T_d (str.++ T1_21 T2_21)))
(assert (= T2_21 (str.++ PCTEMP_LHS_6 T3_21)))
(assert (= 0 (str.len T1_21)))
(assert (= I1_21 (str.len T_d)))
(assert (= T_f PCTEMP_LHS_4_idx_0))
(assert (= T_10 (+ PCTEMP_LHS_5 1)))
(assert (= I0_25 (- I2_25 T_10)))
(assert (>= T_10 0))
(assert (>= I2_25 T_10))
(assert (<= I2_25 I1_25))
(assert (= I2_25 I1_25))
(assert (= I0_25 (str.len PCTEMP_LHS_7)))
(assert (= T_f (str.++ T1_25 T2_25)))
(assert (= T2_25 (str.++ PCTEMP_LHS_7 T3_25)))
(assert (= T_10 (str.len T1_25)))
(assert (= I1_25 (str.len T_f)))
(assert (not (str.in.re PCTEMP_LHS_8 (str.to.re "+"))))
(assert (= PCTEMP_LHS_8 PCTEMP_LHS_7))
(assert (= PCTEMP_LHS_9 PCTEMP_LHS_8))
(assert (not (str.in.re PCTEMP_LHS_9 (str.to.re "%"))))
(assert (= T_14 (str.len PCTEMP_LHS_4)))
(assert (= T_15 (< 1 T_14)))
(assert T_15)
(assert (= T_16 PCTEMP_LHS_4_idx_1))
(assert (= T_SELECT_4 (not (= PCTEMP_LHS_10 (- 1)))))
(assert (ite T_SELECT_4
	(and (= PCTEMP_LHS_10 (+ I0_35 0))(= T_16 (str.++ T0_35 T1_35))(= I0_35 (str.len T4_35))(= 0 (str.len T0_35))(= T1_35 (str.++ T2_35 T3_35))(= T2_35 (str.++ T4_35 T5_35))(= T5_35 "=")(not (str.in.re T4_35 (str.to.re "="))))
	(and (= PCTEMP_LHS_10 (- 1))(= T_16 (str.++ T0_35 T1_35))(= 0 (str.len T0_35))(not (str.in.re T1_35 (str.to.re "="))))))
(assert (= T_18 (= PCTEMP_LHS_10 (- 1))))
(assert T_18)

(check-sat)

